(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const r3 Real)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const r4 Real)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const r5 Real)
(declare-const r6 Real)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const r7 Real)
(declare-const v17 Bool)
(declare-const v18 Bool)
(assert (or v13 (>= r0 r0 r2 r0 r1) (distinct (- r0) r1)))
(assert (or v14 (> r6 (- r1) r3 r6) v1))
(assert (or v17 (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) v18 (>= r6 (+ r0 r2))))
(assert (or (>= r6 (+ r0 r2)) (> r6 (- r1) r3 r6) v6))
(assert (or v13 v16 v16))
(assert (or v16 (>= r0 r0 r2 r0 r1) v13))
(assert (or (< (+ r0 r2) r4 r0) v17 (distinct (- r0) r1)))
(assert (or (> r1 r3 r4 (- 297.73)) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (>= r0 r0 r2 r0 r1)))
(assert (or (> r6 (- r1) r3 r6) (distinct (- r0) r1) v18))
(assert (or v12 (> r1 r3 r4 (- 297.73)) v11))
(assert (or v18 (< (+ r0 r2) r4 r0) v1))
(assert (or v17 (>= r6 (+ r0 r2)) (>= r0 r0 r2 r0 r1)))
(assert (or v17 v16 (> r6 (- r1) r3 r6)))
(assert (or v16 (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) v1))
(assert (or v14 (> r6 (- r1) r3 r6) v11))
(assert (or v17 v16 v17))
(assert (or v11 v11 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or v1 v14 v16))
(assert (or (< (+ r0 r2) r4 r0) (> r1 r3 r4 (- 297.73)) v14))
(assert (or (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (>= (+ r0 r2) r1 r1 r3) (>= r0 r0 r2 r0 r1)))
(assert (or (distinct (- r0) r1) (>= (+ r0 r2) r1 r1 r3) v17))
(assert (or (> r6 (- r1) r3 r6) v12 (>= r6 (+ r0 r2))))
(assert (or (> r6 (- r1) r3 r6) v16 v12))
(assert (or (>= r0 r0 r2 r0 r1) (distinct (- r0) r1) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or (distinct (- r0) r1) (> r6 (- r1) r3 r6) (> r1 r3 r4 (- 297.73))))
(assert (or (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) v13 (< (+ r0 r2) r4 r0)))
(assert (or (< (+ r0 r2) r4 r0) (> r6 (- r1) r3 r6) (> r1 r3 r4 (- 297.73))))
(assert (or (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) v17 v6))
(assert (or (>= r6 (+ r0 r2)) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14)))
(assert (or v1 v12 (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14)))
(assert (or (< (+ r0 r2) r4 r0) v17 v11))
(assert (or (distinct (- r0) r1) v6 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or v13 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (> r6 (- r1) r3 r6)))
(assert (or (>= r0 r0 r2 r0 r1) (< (+ r0 r2) r4 r0) (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14)))
(assert (or v16 (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or v11 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) v13))
(assert (or v12 (>= (+ r0 r2) r1 r1 r3) (< (+ r0 r2) r4 r0)))
(assert (or v18 (>= r6 (+ r0 r2)) v16))
(assert (or v18 v18 (>= r6 (+ r0 r2))))
(assert (or (>= (+ r0 r2) r1 r1 r3) v6 v12))
(assert (or (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (>= (+ r0 r2) r1 r1 r3) (> r6 (- r1) r3 r6)))
(assert (or v17 (> r1 r3 r4 (- 297.73)) (distinct (- r0) r1)))
(assert (or v14 (< (+ r0 r2) r4 r0) v1))
(assert (or (> r6 (- r1) r3 r6) (distinct (- r0) r1) v16))
(assert (or (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) (>= r0 r0 r2 r0 r1) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or (> r6 (- r1) r3 r6) v14 v1))
(assert (or (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) v16 v16))
(assert (or v14 (> r1 r3 r4 (- 297.73)) v16))
(assert (or (>= (+ r0 r2) r1 r1 r3) (>= (+ r0 r2) r1 r1 r3) v18))
(assert (or v13 v12 v16))
(assert (or (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) v17))
(assert (or v14 (>= (+ r0 r2) r1 r1 r3) (>= r0 r0 r2 r0 r1)))
(assert (or (> r1 r3 r4 (- 297.73)) (>= r0 r0 r2 r0 r1) (> r1 r3 r4 (- 297.73))))
(assert (or v18 v11 (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14)))
(assert (or v18 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) v11))
(assert (or v17 v14 v6))
(assert (or (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) (>= r0 r0 r2 r0 r1) v6))
(assert (or v1 v16 (> r6 (- r1) r3 r6)))
(assert (or (distinct (- r0) r1) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (>= r0 r0 r2 r0 r1)))
(assert (or v6 v13 (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14)))
(assert (or v14 v18 (>= r0 r0 r2 r0 r1)))
(assert (or v17 v1 v12))
(assert (or v1 v6 v6))
(assert (or v14 (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14) (>= (+ r0 r2) r1 r1 r3)))
(assert (or (> r1 r3 r4 (- 297.73)) (>= (+ r0 r2) r1 r1 r3) v16))
(assert (or v14 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (< (+ r0 r2) r4 r0)))
(assert (or (distinct (- r0) r1) (>= (+ r0 r2) r1 r1 r3) (> r1 r3 r4 (- 297.73))))
(assert (or (< (+ r0 r2) r4 r0) v11 v6))
(assert (or v13 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) v16))
(assert (or v17 v13 v1))
(assert (or (< (+ r0 r2) r4 r0) v12 (< (+ r0 r2) r4 r0)))
(assert (or v17 v14 (>= r0 r0 r2 r0 r1)))
(assert (or v1 v17 v17))
(assert (or v13 (>= (+ r0 r2) r1 r1 r3) v13))
(assert (or v14 v6 (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2) (distinct (- r0) r1) v1))
(assert (or v12 (< (+ r0 r2) r4 r0) (> r1 r3 r4 (- 297.73))))
(assert (or (>= (+ r0 r2) r1 r1 r3) (< (+ r0 r2) r4 r0) v13))
(assert (or v6 (>= (+ r0 r2) r1 r1 r3) (and (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) v0 (> r6 (- r1) r3 r6) (< (+ r0 r2) r4 r0) (xor (>= (+ r0 r2) r1 r1 r3) (and v3 (<= r0 (+ r0 r2)) v5 v2 v9) v3 (> r1 r1 r4) v6) (> r1 r1 r4) v14)))
(assert (or v6 v6 v17))
(assert (or (< (+ r0 r2) r4 r0) (>= (+ r0 r2) r1 r1 r3) v17))
(assert (or v12 v11 v12))
(assert (or (> r1 r3 r4 (- 297.73)) (> r1 r3 r4 (- 297.73)) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or v1 v11 v6))
(assert (or v17 (>= r6 (+ r0 r2)) v6))
(assert (or v18 (>= (+ r0 r2) r1 r1 r3) v13))
(assert (or v12 v11 (> r1 r3 r4 (- 297.73))))
(assert (or v11 (> r6 (- r1) r3 r6) (distinct v0 v3 (<= r0 (+ r0 r2)) (>= r0 r4 (+ r0 r1 r0) (+ r0 r2)) v9 v0 v10 v0 (or (> r1 r1 r4) v9 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (= (- r1) r4 (+ r0 r1 r0)) (>= r3 r4 (- r1) (+ r0 r2) (- r1)) v2 v7 (= (- r1) r4 (+ r0 r1 r0)) v5 (>= r3 r4 (- r1) (+ r0 r2) (- r1)) (>= r0 r0 r2 r0 r1)) v10 v2)))
(assert (or v13 v11 (>= r0 r0 r2 r0 r1)))
(minimize r0)
(maximize r1)
(minimize r2)
(maximize r5)
(minimize r6)
(minimize r7)
(check-sat)
(exit)
